ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), a,b:update-spec(ds; da).
update-spec-join(a; b)  update-spec(ds; da) 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), fpf(A; a.B(a)), Knd, x:A  B(x), void, x.A(x), t.2, id-deq, fpf-cap(f; eq; x; z), t.1, ma-valtype(da; k), x:AB(x), decl-state(ds), , type List, Kind-deq, product-deq(A; B; a; b), fpf-join(eq; f; g), update-spec-join(a; b), update-spec(ds; da)
Lemmas	fpf-join wf, product-deq wf, Kind-deq wf, nat wf, decl-state wf, ma-valtype wf, pi1 wf, fpf-cap wf, id-deq wf, pi2 wf, Knd wf, fpf wf, Id wf